/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import category_theory.limits.types
import category_theory.limits.shapes.products
import category_theory.limits.shapes.binary_products
import category_theory.limits.shapes.terminal
import category_theory.concrete_category.basic
import tactic.elementwise

/-!
# Special shapes for limits in `Type`.

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

The general shape (co)limits defined in `category_theory.limits.types`
are intended for use through the limits API,
and the actual implementation should mostly be considered "sealed".

In this file, we provide definitions of the "standard" special shapes of limits in `Type`,
giving the expected definitional implementation:
* the terminal object is `punit`
* the binary product of `X` and `Y` is `X × Y`
* the product of a family `f : J → Type` is `Π j, f j`
* the coproduct of a family `f : J → Type` is `Σ j, f j`
* the binary coproduct of `X` and `Y` is the sum type `X ⊕ Y`
* the equalizer of a pair of maps `(g, h)` is the subtype `{x : Y // g x = h x}`
* the coequalizer of a pair of maps `(f, g)` is the quotient of `Y` by `∀ x : Y, f x ~ g x`
* the pullback of `f : X ⟶ Z` and `g : Y ⟶ Z` is the subtype `{ p : X × Y // f p.1 = g p.2 }`
  of the product

We first construct terms of `is_limit` and `limit_cone`, and then provide isomorphisms with the
types generated by the `has_limit` API.

As an example, when setting up the monoidal category structure on `Type`
we use the `types_has_terminal` and `types_has_binary_products` instances.
-/

universes u v

open category_theory
open category_theory.limits

namespace category_theory.limits.types

local attribute [tidy] tactic.discrete_cases

/-- A restatement of `types.lift_π_apply` that uses `pi.π` and `pi.lift`. -/
@[simp]
lemma pi_lift_π_apply
  {β : Type u} (f : β → Type u) {P : Type u} (s : Π b, P ⟶ f b) (b : β) (x : P) :
  (pi.π f b : (∏ f) → f b) (@pi.lift β _ _ f _ P s x) = s b x :=
congr_fun (limit.lift_π (fan.mk P s) ⟨b⟩) x

/-- A restatement of `types.map_π_apply` that uses `pi.π` and `pi.map`. -/
@[simp]
lemma pi_map_π_apply {β : Type u} {f g : β → Type u} (α : Π j, f j ⟶ g j) (b : β) (x) :
  (pi.π g b : (∏ g) → g b) (pi.map α x) = α b ((pi.π f b : (∏ f) → f b) x) :=
limit.map_π_apply _ _ _

/-- The category of types has `punit` as a terminal object. -/
def terminal_limit_cone : limits.limit_cone (functor.empty (Type u)) :=
{ cone :=
  { X := punit,
    π := by tidy, },
  is_limit := by tidy, }

/-- The terminal object in `Type u` is `punit`. -/
noncomputable def terminal_iso : ⊤_ (Type u) ≅ punit :=
limit.iso_limit_cone terminal_limit_cone

/-- The terminal object in `Type u` is `punit`. -/
noncomputable
def is_terminal_punit : is_terminal (punit : Type u) :=
terminal_is_terminal.of_iso terminal_iso

/-- The category of types has `pempty` as an initial object. -/
def initial_colimit_cocone : limits.colimit_cocone (functor.empty (Type u)) :=
{ cocone :=
  { X := pempty,
    ι := by tidy, },
  is_colimit := by tidy, }

/-- The initial object in `Type u` is `pempty`. -/
noncomputable def initial_iso : ⊥_ (Type u) ≅ pempty :=
colimit.iso_colimit_cocone initial_colimit_cocone

/-- The initial object in `Type u` is `pempty`. -/
noncomputable
def is_initial_punit : is_initial (pempty : Type u) :=
initial_is_initial.of_iso initial_iso

open category_theory.limits.walking_pair

/-- The product type `X × Y` forms a cone for the binary product of `X` and `Y`. -/
-- We manually generate the other projection lemmas since the simp-normal form for the legs is
-- otherwise not created correctly.
@[simps X]
def binary_product_cone (X Y : Type u) : binary_fan X Y :=
binary_fan.mk prod.fst prod.snd

@[simp]
lemma binary_product_cone_fst (X Y : Type u) :
  (binary_product_cone X Y).fst = prod.fst :=
rfl
@[simp]
lemma binary_product_cone_snd (X Y : Type u) :
  (binary_product_cone X Y).snd = prod.snd :=
rfl

/-- The product type `X × Y` is a binary product for `X` and `Y`. -/
@[simps]
def binary_product_limit (X Y : Type u) : is_limit (binary_product_cone X Y) :=
{ lift := λ (s : binary_fan X Y) x, (s.fst x, s.snd x),
  fac' := λ s j, discrete.rec_on j (λ j, walking_pair.cases_on j rfl rfl),
  uniq' := λ s m w, funext $ λ x, prod.ext (congr_fun (w ⟨left⟩) x) (congr_fun (w ⟨right⟩) x) }

/--
The category of types has `X × Y`, the usual cartesian product,
as the binary product of `X` and `Y`.
-/
@[simps]
def binary_product_limit_cone (X Y : Type u) : limits.limit_cone (pair X Y) :=
⟨_, binary_product_limit X Y⟩

/-- The categorical binary product in `Type u` is cartesian product. -/
noncomputable def binary_product_iso (X Y : Type u) : limits.prod X Y ≅ X × Y :=
limit.iso_limit_cone (binary_product_limit_cone X Y)

@[simp, elementwise] lemma binary_product_iso_hom_comp_fst (X Y : Type u) :
  (binary_product_iso X Y).hom ≫ prod.fst = limits.prod.fst :=
limit.iso_limit_cone_hom_π (binary_product_limit_cone X Y) ⟨walking_pair.left⟩

@[simp, elementwise] lemma binary_product_iso_hom_comp_snd (X Y : Type u) :
  (binary_product_iso X Y).hom ≫ prod.snd = limits.prod.snd :=
limit.iso_limit_cone_hom_π (binary_product_limit_cone X Y) ⟨walking_pair.right⟩

@[simp, elementwise] lemma binary_product_iso_inv_comp_fst (X Y : Type u) :
  (binary_product_iso X Y).inv ≫ limits.prod.fst = prod.fst :=
limit.iso_limit_cone_inv_π (binary_product_limit_cone X Y) ⟨walking_pair.left⟩

@[simp, elementwise] lemma binary_product_iso_inv_comp_snd (X Y : Type u) :
  (binary_product_iso X Y).inv ≫ limits.prod.snd = prod.snd :=
limit.iso_limit_cone_inv_π (binary_product_limit_cone X Y) ⟨walking_pair.right⟩

/-- The functor which sends `X, Y` to the product type `X × Y`. -/
-- We add the option `type_md` to tell `@[simps]` to not treat homomorphisms `X ⟶ Y` in `Type*` as
-- a function type
@[simps {type_md := reducible}]
def binary_product_functor : Type u ⥤ Type u ⥤ Type u :=
{ obj := λ X,
  { obj := λ Y, X × Y,
    map := λ Y₁ Y₂ f, (binary_product_limit X Y₂).lift (binary_fan.mk prod.fst (prod.snd ≫ f)) },
  map := λ X₁ X₂ f,
  { app := λ Y, (binary_product_limit X₂ Y).lift (binary_fan.mk (prod.fst ≫ f) prod.snd) } }

/--
The product functor given by the instance `has_binary_products (Type u)` is isomorphic to the
explicit binary product functor given by the product type.
-/
noncomputable def binary_product_iso_prod : binary_product_functor ≅ (prod.functor : Type u ⥤ _) :=
begin
  apply nat_iso.of_components (λ X, _) _,
  { apply nat_iso.of_components (λ Y, _) _,
    { exact ((limit.is_limit _).cone_point_unique_up_to_iso (binary_product_limit X Y)).symm },
    { intros Y₁ Y₂ f,
      ext1;
      simp } },
  { intros X₁ X₂ g,
    ext : 3;
    simp }
end

/-- The sum type `X ⊕ Y` forms a cocone for the binary coproduct of `X` and `Y`. -/
@[simps]
def binary_coproduct_cocone (X Y : Type u) : cocone (pair X Y) :=
binary_cofan.mk sum.inl sum.inr

/-- The sum type `X ⊕ Y` is a binary coproduct for `X` and `Y`. -/
@[simps]
def binary_coproduct_colimit (X Y : Type u) : is_colimit (binary_coproduct_cocone X Y) :=
{ desc := λ (s : binary_cofan X Y), sum.elim s.inl s.inr,
  fac' := λ s j, discrete.rec_on j (λ j, walking_pair.cases_on j rfl rfl),
  uniq' := λ s m w, funext $ λ x, sum.cases_on x (congr_fun (w ⟨left⟩)) (congr_fun (w ⟨right⟩)) }

/--
The category of types has `X ⊕ Y`,
as the binary coproduct of `X` and `Y`.
-/
def binary_coproduct_colimit_cocone (X Y : Type u) : limits.colimit_cocone (pair X Y) :=
⟨_, binary_coproduct_colimit X Y⟩

/-- The categorical binary coproduct in `Type u` is the sum `X ⊕ Y`. -/
noncomputable def binary_coproduct_iso (X Y : Type u) : limits.coprod X Y ≅ X ⊕ Y :=
colimit.iso_colimit_cocone (binary_coproduct_colimit_cocone X Y)

open_locale category_theory.Type

@[simp, elementwise] lemma binary_coproduct_iso_inl_comp_hom (X Y : Type u) :
  limits.coprod.inl ≫ (binary_coproduct_iso X Y).hom = sum.inl :=
colimit.iso_colimit_cocone_ι_hom (binary_coproduct_colimit_cocone X Y) ⟨walking_pair.left⟩

@[simp, elementwise] lemma binary_coproduct_iso_inr_comp_hom (X Y : Type u) :
  limits.coprod.inr ≫ (binary_coproduct_iso X Y).hom = sum.inr :=
colimit.iso_colimit_cocone_ι_hom (binary_coproduct_colimit_cocone X Y) ⟨walking_pair.right⟩

@[simp, elementwise] lemma binary_coproduct_iso_inl_comp_inv (X Y : Type u) :
  ↾(sum.inl : X ⟶ X ⊕ Y) ≫ (binary_coproduct_iso X Y).inv = limits.coprod.inl :=
colimit.iso_colimit_cocone_ι_inv (binary_coproduct_colimit_cocone X Y) ⟨walking_pair.left⟩

@[simp, elementwise] lemma binary_coproduct_iso_inr_comp_inv (X Y : Type u) :
  ↾(sum.inr : Y ⟶ X ⊕ Y) ≫ (binary_coproduct_iso X Y).inv = limits.coprod.inr :=
colimit.iso_colimit_cocone_ι_inv (binary_coproduct_colimit_cocone X Y) ⟨walking_pair.right⟩

open function (injective)

lemma binary_cofan_is_colimit_iff {X Y : Type u} (c : binary_cofan X Y) :
  nonempty (is_colimit c) ↔
    injective c.inl ∧ injective c.inr ∧ is_compl (set.range c.inl) (set.range c.inr) :=
begin
  classical,
  split,
  { rintro ⟨h⟩,
    rw [← show _ = c.inl, from h.comp_cocone_point_unique_up_to_iso_inv
      (binary_coproduct_colimit X Y) ⟨walking_pair.left⟩,
      ← show _ = c.inr, from h.comp_cocone_point_unique_up_to_iso_inv
      (binary_coproduct_colimit X Y) ⟨walking_pair.right⟩],
    dsimp [binary_coproduct_cocone],
    refine
    ⟨(h.cocone_point_unique_up_to_iso (binary_coproduct_colimit X Y)).symm.to_equiv.injective.comp
      sum.inl_injective, (h.cocone_point_unique_up_to_iso (binary_coproduct_colimit X Y)).symm
      .to_equiv.injective.comp sum.inr_injective, _⟩,
    erw [set.range_comp, ← eq_compl_iff_is_compl, set.range_comp _ sum.inr, ← set.image_compl_eq
      (h.cocone_point_unique_up_to_iso (binary_coproduct_colimit X Y)).symm.to_equiv.bijective],
    congr' 1,
    exact set.compl_range_inr.symm },
  { rintros ⟨h₁, h₂, h₃⟩,
    have : ∀ x, x ∈ set.range c.inl ∨ x ∈ set.range c.inr,
    { rw [eq_compl_iff_is_compl.mpr h₃.symm], exact λ _, or_not },
    refine ⟨binary_cofan.is_colimit.mk _ _ _ _ _⟩,
    { intros T f g x,
      exact if h : x ∈ set.range c.inl
        then f ((equiv.of_injective _ h₁).symm ⟨x, h⟩)
        else g ((equiv.of_injective _ h₂).symm ⟨x, (this x).resolve_left h⟩) },
    { intros T f g, ext x, dsimp, simp [h₁.eq_iff] },
    { intros T f g, ext x, dsimp,
      simp only [forall_exists_index, equiv.of_injective_symm_apply,
        dif_ctx_congr, dite_eq_right_iff],
      intros y e,
      have : c.inr x ∈ set.range c.inl ⊓ set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩,
      rw disjoint_iff.mp h₃.1 at this,
      exact this.elim },
    { rintro T _ _ m rfl rfl, ext x, dsimp,
      split_ifs; exact congr_arg _ (equiv.apply_of_injective_symm _ ⟨_, _⟩).symm } }
end

/-- Any monomorphism in `Type` is an coproduct injection. -/
noncomputable
def is_coprod_of_mono {X Y : Type u} (f : X ⟶ Y) [mono f] :
  is_colimit (binary_cofan.mk f (subtype.val : (set.range f)ᶜ → Y)) :=
nonempty.some $ (binary_cofan_is_colimit_iff _).mpr
  ⟨(mono_iff_injective f).mp infer_instance, subtype.val_injective,
    (eq_compl_iff_is_compl.mp $ subtype.range_val).symm⟩

/--
The category of types has `Π j, f j` as the product of a type family `f : J → Type`.
-/
def product_limit_cone {J : Type u} (F : J → Type (max u v)) :
  limits.limit_cone (discrete.functor F) :=
{ cone :=
  { X := Π j, F j,
    π := { app := λ j f, f j.as }, },
  is_limit :=
  { lift := λ s x j, s.π.app ⟨j⟩ x,
    uniq' := λ s m w, funext $ λ x, funext $ λ j, (congr_fun (w ⟨j⟩) x : _) } }

/-- The categorical product in `Type u` is the type theoretic product `Π j, F j`. -/
noncomputable def product_iso {J : Type u} (F : J → Type (max u v)) : ∏ F ≅ Π j, F j :=
limit.iso_limit_cone (product_limit_cone F)

@[simp, elementwise] lemma product_iso_hom_comp_eval {J : Type u} (F : J → Type (max u v)) (j : J) :
  (product_iso F).hom ≫ (λ f, f j) = pi.π F j :=
rfl

@[simp, elementwise] lemma product_iso_inv_comp_π {J : Type u} (F : J → Type (max u v)) (j : J) :
  (product_iso F).inv ≫ pi.π F j = (λ f, f j) :=
limit.iso_limit_cone_inv_π (product_limit_cone F) ⟨j⟩

/--
The category of types has `Σ j, f j` as the coproduct of a type family `f : J → Type`.
-/
def coproduct_colimit_cocone {J : Type u} (F : J → Type u) :
  limits.colimit_cocone (discrete.functor F) :=
{ cocone :=
  { X := Σ j, F j,
    ι :=
    { app := λ j x, ⟨j.as, x⟩ }, },
  is_colimit :=
  { desc := λ s x, s.ι.app ⟨x.1⟩ x.2,
    uniq' := λ s m w,
    begin
      ext ⟨j, x⟩,
      have := congr_fun (w ⟨j⟩) x,
      exact this,
    end }, }

/-- The categorical coproduct in `Type u` is the type theoretic coproduct `Σ j, F j`. -/
noncomputable def coproduct_iso {J : Type u} (F : J → Type u) : ∐ F ≅ Σ j, F j :=
colimit.iso_colimit_cocone (coproduct_colimit_cocone F)

@[simp, elementwise] lemma coproduct_iso_ι_comp_hom {J : Type u} (F : J → Type u) (j : J) :
  sigma.ι F j ≫ (coproduct_iso F).hom = (λ x : F j, (⟨j, x⟩ : Σ j, F j)) :=
colimit.iso_colimit_cocone_ι_hom (coproduct_colimit_cocone F) ⟨j⟩

@[simp, elementwise] lemma coproduct_iso_mk_comp_inv {J : Type u} (F : J → Type u) (j : J) :
  ↾(λ x : F j, (⟨j, x⟩ : Σ j, F j)) ≫ (coproduct_iso F).inv = sigma.ι F j :=
rfl

section fork
variables {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : f ≫ g = f ≫ h)

/--
Show the given fork in `Type u` is an equalizer given that any element in the "difference kernel"
comes from `X`.
The converse of `unique_of_type_equalizer`.
-/
noncomputable def type_equalizer_of_unique (t : ∀ (y : Y), g y = h y → ∃! (x : X), f x = y) :
  is_limit (fork.of_ι _ w) :=
fork.is_limit.mk' _ $ λ s,
begin
  refine ⟨λ i, _, _, _⟩,
  { apply classical.some (t (s.ι i) _),
    apply congr_fun s.condition i },
  { ext i,
    apply (classical.some_spec (t (s.ι i) _)).1 },
  { intros m hm,
    ext i,
    apply (classical.some_spec (t (s.ι i) _)).2,
    apply congr_fun hm i },
end

/-- The converse of `type_equalizer_of_unique`. -/
lemma unique_of_type_equalizer (t : is_limit (fork.of_ι _ w)) (y : Y) (hy : g y = h y) :
  ∃! (x : X), f x = y :=
begin
  let y' : punit ⟶ Y := λ _, y,
  have hy' : y' ≫ g = y' ≫ h := funext (λ _, hy),
  refine ⟨(fork.is_limit.lift' t _ hy').1 ⟨⟩, congr_fun (fork.is_limit.lift' t y' _).2 ⟨⟩, _⟩,
  intros x' hx',
  suffices : (λ (_ : punit), x') = (fork.is_limit.lift' t y' hy').1,
    rw ← this,
  apply fork.is_limit.hom_ext t,
  ext ⟨⟩,
  apply hx'.trans (congr_fun (fork.is_limit.lift' t _ hy').2 ⟨⟩).symm,
end

lemma type_equalizer_iff_unique :
  nonempty (is_limit (fork.of_ι _ w)) ↔ (∀ (y : Y), g y = h y → ∃! (x : X), f x = y) :=
⟨λ i, unique_of_type_equalizer _ _ (classical.choice i), λ k, ⟨type_equalizer_of_unique f w k⟩⟩

/-- Show that the subtype `{x : Y // g x = h x}` is an equalizer for the pair `(g,h)`. -/
def equalizer_limit : limits.limit_cone (parallel_pair g h) :=
{ cone := fork.of_ι (subtype.val : {x : Y // g x = h x} → Y) (funext subtype.prop),
  is_limit := fork.is_limit.mk' _ $ λ s,
    ⟨λ i, ⟨s.ι i, by apply congr_fun s.condition i⟩,
     rfl,
     λ m hm, funext $ λ x, subtype.ext (congr_fun hm x)⟩ }

variables (g h)

/-- The categorical equalizer in `Type u` is `{x : Y // g x = h x}`. -/
noncomputable def equalizer_iso : equalizer g h ≅ {x : Y // g x = h x} :=
limit.iso_limit_cone equalizer_limit

@[simp, elementwise] lemma equalizer_iso_hom_comp_subtype :
  (equalizer_iso g h).hom ≫ subtype.val = equalizer.ι g h :=
rfl

@[simp, elementwise] lemma equalizer_iso_inv_comp_ι :
  (equalizer_iso g h).inv ≫ equalizer.ι g h = subtype.val :=
limit.iso_limit_cone_inv_π equalizer_limit walking_parallel_pair.zero

end fork

section cofork
variables {X Y Z : Type u} (f g : X ⟶ Y)

/-- (Implementation) The relation to be quotiented to obtain the coequalizer. -/
inductive coequalizer_rel : Y → Y → Prop
| rel (x : X) : coequalizer_rel (f x) (g x)

/--
Show that the quotient by the relation generated by `f(x) ~ g(x)`
is a coequalizer for the pair `(f, g)`.
-/
def coequalizer_colimit : limits.colimit_cocone (parallel_pair f g) :=
{ cocone := cofork.of_π (quot.mk (coequalizer_rel f g))
    (funext (λ x, quot.sound (coequalizer_rel.rel x))),
  is_colimit := cofork.is_colimit.mk' _ $ λ s,
    ⟨ quot.lift s.π (λ a b (h : coequalizer_rel f g a b),
        by { cases h, exact congr_fun s.condition h_1 }),
      rfl,
      λ m hm, funext $ λ x, quot.induction_on x (congr_fun hm : _) ⟩ }

/-- If `π : Y ⟶ Z` is an equalizer for `(f, g)`, and `U ⊆ Y` such that `f ⁻¹' U = g ⁻¹' U`,
then `π ⁻¹' (π '' U) = U`.
-/
lemma coequalizer_preimage_image_eq_of_preimage_eq (π : Y ⟶ Z)
  (e : f ≫ π = g ≫ π) (h : is_colimit (cofork.of_π π e)) (U : set Y) (H : f ⁻¹' U = g ⁻¹' U) :
    π ⁻¹' (π '' U) = U :=
begin
  have lem : ∀ x y, (coequalizer_rel f g x y) → (x ∈ U ↔ y ∈ U),
  { rintros _ _ ⟨x⟩, change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U, congr' 2 },
  have eqv : _root_.equivalence (λ x y, x ∈ U ↔ y ∈ U) := by tidy,
  ext,
  split,
  { rw ← (show _ = π, from h.comp_cocone_point_unique_up_to_iso_inv
      (coequalizer_colimit f g).2 walking_parallel_pair.one),
    rintro ⟨y, hy, e'⟩,
    dsimp at e',
    replace e' := (mono_iff_injective (h.cocone_point_unique_up_to_iso
      (coequalizer_colimit f g).is_colimit).inv).mp infer_instance e',
    exact (eqv.eqv_gen_iff.mp (eqv_gen.mono lem (quot.exact _ e'))).mp hy },
  { exact λ hx, ⟨x, hx, rfl⟩ }
end

/-- The categorical coequalizer in `Type u` is the quotient by `f g ~ g x`. -/
noncomputable def coequalizer_iso : coequalizer f g ≅ _root_.quot (coequalizer_rel f g) :=
colimit.iso_colimit_cocone (coequalizer_colimit f g)

@[simp, elementwise] lemma coequalizer_iso_π_comp_hom :
  coequalizer.π f g ≫ (coequalizer_iso f g).hom = quot.mk (coequalizer_rel f g) :=
colimit.iso_colimit_cocone_ι_hom (coequalizer_colimit f g) walking_parallel_pair.one

@[simp, elementwise] lemma coequalizer_iso_quot_comp_inv :
  ↾(quot.mk (coequalizer_rel f g)) ≫ (coequalizer_iso f g).inv = coequalizer.π f g :=
rfl

end cofork

section pullback
open category_theory.limits.walking_pair
open category_theory.limits.walking_cospan
open category_theory.limits.walking_cospan.hom

variables {W X Y Z : Type u}
variables (f : X ⟶ Z) (g : Y ⟶ Z)

/--
The usual explicit pullback in the category of types, as a subtype of the product.
The full `limit_cone` data is bundled as `pullback_limit_cone f g`.
-/
@[nolint has_nonempty_instance]
abbreviation pullback_obj : Type u := { p : X × Y // f p.1 = g p.2 }

-- `pullback_obj f g` comes with a coercion to the product type `X × Y`.
example (p : pullback_obj f g) : X × Y := p

/--
The explicit pullback cone on `pullback_obj f g`.
This is bundled with the `is_limit` data as `pullback_limit_cone f g`.
-/
abbreviation pullback_cone : limits.pullback_cone f g :=
pullback_cone.mk (λ p : pullback_obj f g, p.1.1) (λ p, p.1.2) (funext (λ p, p.2))

/--
The explicit pullback in the category of types, bundled up as a `limit_cone`
for given `f` and `g`.
-/
@[simps]
def pullback_limit_cone (f : X ⟶ Z) (g : Y ⟶ Z) : limits.limit_cone (cospan f g) :=
{ cone := pullback_cone f g,
  is_limit := pullback_cone.is_limit_aux _
    (λ s x, ⟨⟨s.fst x, s.snd x⟩, congr_fun s.condition x⟩)
    (by tidy)
    (by tidy)
    (λ s m w, funext $ λ x, subtype.ext $
     prod.ext (congr_fun (w walking_cospan.left) x)
              (congr_fun (w walking_cospan.right) x)) }

/--
The pullback cone given by the instance `has_pullbacks (Type u)` is isomorphic to the
explicit pullback cone given by `pullback_limit_cone`.
-/
noncomputable def pullback_cone_iso_pullback : limit.cone (cospan f g) ≅ pullback_cone f g :=
(limit.is_limit _).unique_up_to_iso (pullback_limit_cone f g).is_limit

/--
The pullback given by the instance `has_pullbacks (Type u)` is isomorphic to the
explicit pullback object given by `pullback_limit_obj`.
-/
noncomputable def pullback_iso_pullback : pullback f g ≅ pullback_obj f g :=
(cones.forget _).map_iso $ pullback_cone_iso_pullback f g

@[simp] lemma pullback_iso_pullback_hom_fst (p : pullback f g) :
  ((pullback_iso_pullback f g).hom p : X × Y).fst = (pullback.fst : _ ⟶ X) p :=
congr_fun ((pullback_cone_iso_pullback f g).hom.w left) p

@[simp] lemma pullback_iso_pullback_hom_snd (p : pullback f g) :
  ((pullback_iso_pullback f g).hom p : X × Y).snd = (pullback.snd : _ ⟶ Y) p :=
congr_fun ((pullback_cone_iso_pullback f g).hom.w right) p

@[simp] lemma pullback_iso_pullback_inv_fst :
  (pullback_iso_pullback f g).inv ≫ pullback.fst = (λ p, (p : X × Y).fst) :=
(pullback_cone_iso_pullback f g).inv.w left

@[simp] lemma pullback_iso_pullback_inv_snd :
  (pullback_iso_pullback f g).inv ≫ pullback.snd = (λ p, (p : X × Y).snd) :=
(pullback_cone_iso_pullback f g).inv.w right

end pullback

end category_theory.limits.types
